$\forall$$P$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $p$:es{-}real\{i:l\}(${\it es}$.$P$(${\it es}$)). es{-}realizer($p$) $\in$ es\_realizer\{i:l\}